Various methods and tools are known in the art for verifying computer programs. Some methods and tools use explicit model checking, which explicitly represents and traverses a state space representation of the computer program. For example, Microsoft Corp. (Redmond, Wash.) offers a software model checking tool called Zing. Zing comprises a modeling language for expressing executable concurrent models of software, a model checking infrastructure for exploring the state space of Zing models, as well as support infrastructure for generating Zing models automatically from common programming languages.
Another example of an explicit model checker is an open source tool called Spin. Spin is described, for example, by Holzmann in “The Model Checker Spin,” IEEE Transactions on Software Engineering, (23:5), May 1997, pages 1-17.
Some software verification tools use symbolic model checking methods, such as methods based on propositional satisfiability (SAT), in which the verified computer program is expressed as a Boolean formula that is evaluated by a SAT solver. For example, Clarke et al. describe a verification tool called C-language Bounded Model Checker (CBMC) in “A Tool for Checking ANSI-C Programs,” Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Barcelona, Spain, Mar. 29-Apr. 2, 2004, pages 168-176.
Some symbolic model checking methods and tools use binary decision diagrams (BDD). For example, Barner et al. describe a BDD-based symbolic model checker in “Wolf—Bug Hunter for Concurrent Software using Formal Methods,” Proceedings of the Seventeenth International Conference on Computer Aided Verification (CAV), Edinburgh, Scotland, UK, Jul. 6-10, 2005, pages 151-157.
Some model checking methods and tools are used for verifying concurrent computer programs. For example, Rabinovitz and Grumberg describe a SAT-based bounded verification technique called Threaded-CBMC (TCBMC), in “Bounded Model Checking of Concurrent Programs,” Proceedings of the Seventeenth International Conference on Computer Aided Verification (CAV), Edinburgh, Scotland, UK, Jul. 6-10, 2005, pages 82-97. TCBMC, which is based on the CBMC tool cited above, performs verification of threaded C programs.
Another symbolic execution method is described by Khurshid et al., in “Generalized Symbolic Execution for Model Checking and Testing,” Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Warsaw, Poland, Apr. 7-11, 2003. First, the program is instrumented with a source-to-source translation. The translation enables standard model checkers to perform symbolic execution of the program. Then, a symbolic execution algorithm that handles dynamically allocated structures, method preconditions, data and concurrency is applied.